Cubical Type Theory
Cubical Type Theory(立方型理論); CubicalTT
HoTTのUnivalence Axiom (UA)を計算可能にした理論らしい
『Cubical Type Theory: a constructive interpretation of the univalence axiom』を読む
1Lab: 1Lab - 1Lab
実装
Cubical Agda
確認用
Q. Cubical Type Theory
関連
Observational Type Theory
Computational Type Theory
メモ
/mrsekut-p/Cubical Type Theory
On Higher Inductive Types in Cubical Type Theory | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
On Higher Inductive Types in Cubical Type Theory
Cubical Type Theory: a constructive interpretation of the univalence axiom. 2016-11-07.
cubical type theory in nLab
Cubical Agda: a cold Introduction – Nextjournal
Type-Theoretic Truncation Levels - YouTube
https://www.youtube.com/watch?v=LWQqE2JcDSQ&list=PL0OBHndHAAZrGQEkOZGyJu7S7KudAJ8M9
masahiro_sakai
Cubical Type Theory は HoTT の univalence axiom をちゃんと計算できる形に解釈できる理論で、直観的にはパスをI=0,1からの関数として解釈する。実装としてはもともとcubicalttという実験的なプロトタイプ実装はあったけど、今回Agdaを拡張してfull-fledgedな実装を提案したという感じ。
Computational Type Theory 【1/5】 - Robert Harper - OPLSS 2018 - YouTube
https://www.youtube.com/watch?v=LE0SSLizYUI&list=PL0DsGHMPLUWXXA8RHzVZ2B5E5hP8CD15Z&index=1
Cubical Type Theory - PKC - Obsidian Publish
調査用
Google.icon Cubical Type Theory(日)
Google.icon Cubical Type Theory(英)
Wikipedia.icon
Cubical Type Theory - Wikipedia(日)
Cubical Type Theory(検索) - Wikipedia(日)
Wikipedia.icon
Cubical Type Theory - Wikipedia(英)
Cubical Type Theory(検索) - Wikipedia(英)